R-Feasible(R)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2 & left || right
== Rinit(loc,T,x,v)=> AtomFree(Type;T)
== Rframe(loc,T,x,L)=> Normal(T)
== Rsframe(lnk,tag,L)=> True
== Reffect(loc,ds,knd,T,x,f)=> Normal(ds) & Normal(T) & (isrcv(knd)  loc = destination(lnk(knd)))
== Rsends(ds,knd,T,l,dt,g)=> (isrcv(knd)
== Rsends(ds,knd,T,l,dt,g)=> ( (lnk(knd) = l  T = dt(tag(knd))?Void)
== Rsends(ds,knd,T,l,dt,g)=> ( & destination(lnk(knd)) = source(l))
== & Normal(T) & Normal(ds)
== & Normal(dt)
== Rpre(loc,ds,a,T,P)=> Normal(T) & Normal(ds) & (s:State(ds). Dec(v:T. P(s,v)))
== Raframe(loc,k,L)=> True
== Rbframe(loc,k,L)=> True
== Rrframe(loc,x,L)=> True 

latex

---

clarification:

R-Feasible{i:l}
R-Feasible(R)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2 & R-compat{i:l}(left; right)
== Rinit(loc,T,x,v)=> AtomFree(Type{i};T)
== Rframe(loc,T,x,L)=> normal-type{i:l}
== Rframe(loc,T,x,L)=> normal-type(T)
== Rsframe(lnk,tag,L)=> True
== Reffect(loc,ds,knd,T,x,f)=> normal-ds{i:l}(ds) & normal-type{i:l}(T)
== & (isrcv(knd)  loc = destination(lnk(knd))  Id)
== Rsends(ds,knd,T,l,dt,g)=> (isrcv(knd)
== Rsends(ds,knd,T,l,dt,g)=> ( (lnk(knd) = l  T = fpf-cap(dt;IdDeq;tag(knd);Void)  Type{i})
== Rsends(ds,knd,T,l,dt,g)=> ( & destination(lnk(knd)) = source(l)  Id)
== & normal-type{i:l}(T) & normal-ds{i:l}(ds)
== & normal-ds{i:l}
== & normal-ds(dt)
== Rpre(loc,ds,a,T,P)=> normal-type{i:l}(T) & normal-ds{i:l}(ds) & (s:State(ds). Dec(v:T. P(s,v)))
== Raframe(loc,k,L)=> True
== Rbframe(loc,k,L)=> True
== Rrframe(loc,x,L)=> True 

latex

Definitions	es realizer ind, A || B, AtomFree(T;x), isrcv(k), P  Q, b, a = b, Type, f(x)?z, IdDeq, tag(k), Void, s = t, Id, destination(l), lnk(k), source(l), Normal(T), P & Q, Normal(ds), x:A. B(x), State(ds), Dec(P), x:A. B(x), f(a), True
FDL editor aliases	R-Feasible